T:Type, a:T, L1, L2:T List. a.L1  L2  L1  L2 

latex

Definitions	x:A. B(x), b, tl(l), A, P  Q, t  T, False, L1  L2
Lemmas	false wf, sublist tl, sublist transitivity, sublist wf, sublist weakening